package trabajoISW2.domain.contracts;

import java.util.List;

import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Query;
import trabajoISW2.domain.implementations.Book;

@Inv("getPublisherId() >= 0")
public interface IPublisher {

	@Pre({"publisherId >= 0 && publisherId <=Integer.MAX_VALUE ##WrongIdException"})
	@Pos("getPublishertId() == publisherId")
	public void setPublisherId (int publisherId);
	
	@Query
	public int getPublisherId ();
	
	@Pre("name.compareTo(\"\") != 0 && name != null #WrongNameException")
	@Pos("getName().compareTo(name) == 0")
	public void setName (String name);
	
	@Query
	public String getName();
	
	@Pre("books !=null #IllegalArgumentException")
	@Pos("getBooks().compare(books) == 0")
	public void setBooks (List<Book> books);
	
	@Query
	public List<Book> getBooks();
	
	@Pre("book != null #IllegalArgumentException")
	@Pos({"!getBooks().contains(book)@pre ==> getBooks().contains(book) && getBooks().size() == getBooks().size()@pre + 1",
		  "getBooks().contains(book)@pre ==> getBooks().size() == getBooks().size()@pre"})
	public void addBook(Book book);
	

	@Pre("book != null #IllegalArgumentException")
	@Pos({"getBooks().contains(book)@pre ==> !getBooks().contains(book) && getBooks().size() == getBooks().size()@pre -1",
		  "!getBooks().contains(book)@pre ==> getBooks().size()@pre == getBooks.size()"})
	public void removeBook(Book book);
	
		
}
